Termination Proof Script
Consider the TRS R consisting of the rewrite rule
1:
g
(
f
(x,y))
→
f
(
f
(
g
(
g
(x)),
g
(
g
(y))),
f
(
g
(
g
(x)),
g
(
g
(y))))
There are 4 dependency pairs:
2:
G
(
f
(x,y))
→
G
(
g
(x))
3:
G
(
f
(x,y))
→
G
(x)
4:
G
(
f
(x,y))
→
G
(
g
(y))
5:
G
(
f
(x,y))
→
G
(y)
Consider the SCC {2-5}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.02 seconds) --- May 3, 2006